\begin{tabbing}
$\vdash$  \=$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $p$:($x$:$A$ $\times$ $B$($x$)), $C$,$D$:Type, $f$:($C$$\rightarrow$$D$), $b$:($x$:$A$$\rightarrow$$B$($x$)$\rightarrow$$C$).\+
\\[0ex]$f$(let $x$,$y$ = $p$ in $b$($x$,$y$)) = let $x$,$y$ = $p$ in $f$($b$($x$,$y$))
\-
\end{tabbing}